Nuprl Definition : strict-fun-connected
11,40
postcript
pdf
y
=
f
+(
x
) == (
(
x
=
y
)) &
y
is
f
*(
x
)
latex
clarification:
strict-fun-connected(
T
;
f
;
x
;
y
) == (
(
x
=
y
T
)) & fun-connected(
T
;
f
;
x
;
y
)
latex
Definitions
P
&
Q
,
A
,
s
=
t
,
y
is
f
*(
x
)
FDL editor aliases
strict-fun-connected
origin
(x = y)) & y is f*(x)
(x = y 
T)) & fun-connected(T;f;x;y) (x = y)) & y is f*(x)
(x = y T)) & fun-connected(T;f;x;y) A